% Created 2020-01-06 一 14:50
% Intended LaTeX compiler: pdflatex
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{grffile}
\usepackage{longtable}
\usepackage{wrapfig}
\usepackage{rotating}
\usepackage[normalem]{ulem}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{amssymb}
\usepackage{capt-of}
\usepackage{hyperref}
\usepackage{minted}
\author{wu}
\date{\today}
\title{}
\hypersetup{
 pdfauthor={wu},
 pdftitle={},
 pdfkeywords={},
 pdfsubject={},
 pdfcreator={Emacs 26.3 (Org mode 9.3)}, 
 pdflang={English}}
\begin{document}

\tableofcontents \clearpage\% Created 2020-01-06 一 14:49
\% Intended \LaTeX{} compiler: pdflatex
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{grffile}
\usepackage{longtable}
\usepackage{wrapfig}
\usepackage{rotating}
\usepackage[normalem]{ulem}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{amssymb}
\usepackage{capt-of}
\usepackage{hyperref}
\usepackage{minted}
\input{preamble.tex}
\usepackage{bussproofs}
\author{A. S. Troelstra and H. Schwichtenberg}
\date{\today}
\title{Basic Proof Theory}
\hypersetup\{
 pdfauthor=\{A. S. Troelstra and H. Schwichtenberg\},
 pdftitle=\{Basic Proof Theory\},
 pdfkeywords=\{\},
 pdfsubject=\{\},
 pdfcreator=\{Emacs 26.3 (Org mode 9.3)\}, 
 pdflang=\{English\}\}
\begin{document}

\maketitle
\tableofcontents \clearpage
\section{Introduction}
\label{sec:org60274b6}
\subsection{Preliminaries}
\label{sec:orgea98477}
\subsubsection{Subformulas}
\label{sec:org97a82a3}
\begin{definition}[]
The notion of \textbf{positive}, \textbf{negative}, \textbf{strictly positive} subformula are defined
in a similar style
\begin{enumerate}
\item \(A\) is a positive and a strictly positive subformula of itself
\item if \(B\wedge C\) or \(B\vee C\) is a positive [negative, strictly positive]
subformula of \(A\), then so are \(B,C\)
\item if \(\forall xB\) or \(\exists xB\) is a positive [negative, strictly
positive] subformula of \(A\), then so is \(B[x/t]\) for any \(t\) free for \(x\)
in \(B\)
\item if \(B\to C\) is a positive [negative] subformula of \(A\), then \(B\) is a
negative [positive] subformula of \(A\), and \(C\) is a positive [negative]
subformula of \(A\)
\item if \(B\to C\) is a strictly positive subformula of \(A\) then so is \(C\)
\end{enumerate}


A strictly positive subformula of \(A\) is called a \textbf{strictly positive part
(s.p.p.)} of \(A\)
\end{definition}
\subsubsection{Contexts and Formula Occurrences}
\label{sec:org1e5c126}
Formula occurrences (f.o.'s) will play an even more important role than the
formulas themselves. An f.o. is nothing but a formula with a position in
another structure (prooftree, sequent, a larger formula etc.).

A \textbf{context} is nothing but a formula with an occurrences of a special
propositional variable. Alternatively, a context is sometimes described as a
formula with a hole in it. 

\begin{definition}[]
We define \textbf{positive} (\(\calp\)) and \textbf{negative (formula-)contexts} (\(\caln\))
simultaneously by an induction definition. The symbol "\(*\)" functions as a
special proposition lett, a \textbf{placeholder}
\begin{enumerate}
\item \(*\in\calp\)
\end{enumerate}


and if \(B^+\in \calp,B^{\minus}\in\caln\) and \(A\) is any formula, then
\begin{enumerate}
\setcounter{enumi}{1}
\item \(A\wedge B^+,B^+\wedge A,A\vee B^+,B^+\vee A,A\to B^+,B^{\minus}\to A,
       \forall xB^+,\exists xB^+\in\calp\)

\item \(A\wedge B^-,B^-\wedge A,A\vee B^-,B^-\vee A,A\to B^-,B^+\to A,
       \forall xB^-,\exists xB^-\in\caln\)
\end{enumerate}


The set of \textbf{formula contexts} is the union of \(\calp\) and \(\caln\). Note that a
context contains always only a single occurrence of \(*\).

For arbitrary contexts we sometimes write \(F[*],G[*],\dots\) THen
\(F[A],G[A],\dots\) are the formulas obtained by replacing \(*\) by \(A\)

The \textbf{strictly positive} contexts \(\cals\calp\) are defined by
\begin{enumerate}
\setcounter{enumi}{3}
\item \(*\in\cals\calp\); and if \(B\in\cals\calp\), then
\item \(A\wedge B,B\wedge A,A\vee B,B\vee A,A\to B,\forall xB,\exists
       xB\in\cals\calp\)
\end{enumerate}


An alternative definition
\begin{align*}
&\calp=*\mid A\wedge\calp\mid\calp\wedge A\mid A\vee\calp\mid\calp\vee A\mid 
A\to\calp\mid\caln\to A\mid\forall x\calp\mid\exists x\calp\\
&\caln=A\wedge\caln\mid\caln\wedge A\mid A\vee\caln\mid\caln\vee A\mid A\to\caln
\mid\calp\to A\mid\forall x\caln\mid \exists x\caln\\
&\cals\calp=*\mid A\wedge\cals\calp\mid\cals\calp\wedge A\mid
A\vee\cals\calp\mid\cals\calp\vee A\mid A\to\cals\calp
\mid\forall x\cals\calp\mid\exists x\cals\calp
\end{align*}

A \textbf{formula occurence} (\textbf{f.o.} for short) in a formula \(B\) is a literal
subformula \(A\) together with a context indicating the place where \(A\) occurs.
\end{definition}

\subsection{Simple type theories}
\label{sec:org316868d}
\begin{definition}[the set of simple types]
the set of \tf{simple types} \(\calt_\to\) is constructed from a countable set
of \tf{type variables} \(P_0,P_1,\dots\) by means of a type-forming operation
(\tf{function-type constructor}) \(\to\)
\begin{enumerate}
\item type variables belong to \(\calt_\to\)
\item if \(A,B\in\calt_\to\), then \((A\to B)\in\calt_\rightarrow\)
\end{enumerate}


A type of the form \(A\to B\) is called a \tf{function type}
\end{definition}

\begin{definition}[Terms of the simply typed lambda calculus $\blambda_{\bto}$]
All terms appear with a type; for terms of type \(A\) we use \(t^A,s^A,r^A\). The
terms are generated by the following three clauses
\begin{enumerate}
\item For each \(A\in T_\to\) there is a countably infinite supply of variables of
type \(A\); for arbitrary variables of type \(A\) we use
\(u^A,v^A,w^A,x^A,y^A,z^A\)
\item if \(t^{A\to B},s^A\) are terms, then \(\app(t^{A\to B},s^A)^B\) is a term of
type \(B\)
\item if \(t^B\) is a term of type \(B\) and \(x^A\) a variable of type \(A\), then
\((\lambda x^A.t^B)^{A\to B}\)
\end{enumerate}
\end{definition}
For \(\app(t^{A\to B},s^A)^B\) we usually write simply \((t^{A\to B}s^A)^B\)
\begin{definition}[]
The set \(\fv(t)\) of variables free in \(t\) is specified by
\begin{alignat*}{2}
&\fv(x^A)&&:=x^A\\
&\fv(ts)&&:=\fv(t)\cup\fv(s)\\
&\fv(\lambda x.t)&&:=\fv(t)\backslash\{x\}
\end{alignat*}
\end{definition}


\begin{definition}[Substitution]
The operation of substitution of a term \(s\) for a variable \(x\) in a term \(t\)
(notation \(t[x/s]\)) may be defined by recursion on the complexity of \(t\), as
follows
\begin{alignat*}{2}
&x[x/s]&&:=s\\
&y[x/s]&&:=y\text{ for } y\not\equiv x\\
&(t_1t_2)[x/s]&&:=t_1[x/s]t_2[x/s]\\
&(\lambda x.t)[x/s]&&:=\lambda x.t\\
&(\lambda y.t)[x/s]&&=\lambda y.t[x/s]\text{ for } y\not\equiv x; \text{
w.l.o.g. } y\not\in\fv(s)
\end{alignat*}
\end{definition}

\begin{lemma}[Substitution lemma]
If \(x\not\equiv y, x\not\in\fv(t_2)\), then
\begin{equation*}
t[x/t_1][y/t_2]\equiv t[y/t_2][x/t_1[y/t_2]]
\end{equation*}
\end{lemma}

\begin{definition}[Conversion, reduction, normal form]
Let \(\mathsf{T}\) be a set of terms, and let conv be a binary relation on
\(\mathsf{T}\), written in infix notation: \(t\) conv \(s\). If \(t\) conv \(s\), we
say that \(t\) \tf{converts to} \(s\); \(t\) is called a \tf{redex} or
\tf{convertible} term and \(s\) the \tf{conversum} of \(t\). The replacement of a
redex by its conversum is called a \tf{conversion}. We write \(t\succ_1 s\)
(\(t\) \tf{reduces in one step to } \(s\)) if \(s\) is obtained from \(t\) by
replacement of a redex \(t'\) of \(t\) by a conversum \(t''\) of \(t'\). The relation
\(\succ\) (\tf{properly reduces to}) is the transitive closure of \(\succ_1\) and
\(\succeq\) (\tf{reduces to}) is the reflexive and transitive closure of
\(\succ_1\). The relation \(\succeq\) is said to be the notion of reduction
\tf{generated} by cont.

With the notion of reduction generated by cony we associate a relation on
\(\mathsf{T}\) called \textbf{conversion equality}: \(t=_{\conv}s\) (\(t\) is equal by
conversion to \(s\)) if there 
is a sequence \(t_0,\dots,t_n\) with \(t_0\equiv t,t_n\equiv s\), and \(t_i\preceq
   t_{i+1}\) or \(t_i\succeq t_{i+1}\) for each
\(i, 0\le i < n\). The subscript "conv" is usually omitted when clear from the
context

A term \(t\) is in \textbf{normal form}, or \(t\) is \textbf{normal}, if \(t\) does not contain a redex. \(t\)
\textbf{has a normal form} if there is a normal \(s\) such that \(t\succeq s\).

A \textbf{reduction sequence} is a (finite or infinite) sequence of pairs
\((t_0,\delta_0),(t_1,\delta_1),\dots\) 
with \(\delta_i\) an (occurrence of a) redex in \(t_i\) and \(t_i\succ t_{i+1}\) by
conversion 
of \(\delta_i\), for all \(i\). This may be written as
\begin{equation*}
t_0\overset{\delta_0}{\succ}_1 t_1\overset{\delta_1}{\succ}_1 t_2
\overset{\delta_2}{\succ}_1\dots
\end{equation*}
We often omit the \(\delta_i\), simply writing \(t_0\succ_1 t_1\succ_1 t_2\)

Finite reduction sequences are partially ordered under the initial part
relation ("sequence \(\sigma\) is an initial part of sequence \(\tau\)"); the collection of
finite 
reduction sequences starting from a term \(g\) forms a tree, the \textbf{reduction tree}
of \(t\). The branches of this tree may be identified with the collection of all
infinite and all terminating finite reduction sequences.


A term is \textbf{strongly normalizing} (is SN) if its reduction tree is finite
\end{definition}

\(\beta\)-conversion:
\begin{equation*}
(\lambda x^A.t^B) s^A\e\cont_\beta\e t^B[x^A/s^A]
\end{equation*}
\(\eta\)-conversion:
\begin{equation*}
\lambda x^A.tx\e\cont_\eta\e  t\quad(x\not\in\fv(t))
\end{equation*}
\(\beta \eta\)-conversion \(\cont_{\beta\eta}\) is \(\cont_\beta\cup\cont_\eta\)

\begin{definition}[]
A relation \(R\) is said to be \textbf{confluent}, or to have the \textbf{Church-Rosser property}
(CR), if whenever \(t_0 Rt_1\) and \(t_0Rt_2\), then there is a \(t_3\) s.t.
\(t_1Rt_3\) and \(t_2Rt_3\). A relation \(R\) is said to be \textbf{weakly confluent} or to
have the \textbf{weak Church-Rosser property} if whenever \(t_0Rt_1,t_0Rt_2\) there is a
\(t_3\) s.t. \(t_1R^*t_3\) and \(t_2R^* t_3\) where \(R^*\) is the reflexive and
transitive closure of \(T\)
\end{definition}

\begin{theorem}[]
For a confluent reduction relation \(\succeq\) the normal forms of terms are
unique. Furthermore, if \(\succeq\) is a confluent reduction relation we have
\(t=t'\) iff there is a term \(t''\) s.t. \(t\succ t''\) and \(t'\succ t''\)
\end{theorem}

\begin{theorem}[Newman's lemma]
Let \(\succeq\) be the transitive and reflexive closure of \(\succ_1\), and let
\(\succ_1\) be weakly confluent. Then the normal form w.r.t. \(\succ_1\) of a
strongly normalizing \(t\) is unique. Moreover, if all terms are strongly
normalizing w.r.t. \(\succ_1\) then the relation \(\succeq\) is confluent.
\end{theorem}

\begin{proof}
Assume WCR, and let write \(s\in UN\) to indicate that \(s\) has a unique normal
form. Assume \(t\in SN, t\not\in UN\). Then there are two reduction sequences
\(t\succ_1 t_1'\dots\succ_1 t'\) and \(t\succ_1 T_1''\succ_1\dots\succ_1 t''\) with
\(t'\not\equiv t''\). Then either \(t'_1=t''_1\) or \(t'_1\neq t_1''\)

In the first case we can take \(t_1:=t_1'=t_1''\). In the second case, by WCR
we can find a \(t^*\) s.t. \(t^*\prec t_1',t_1''\); \(t\in SN\) hence \(t^*\succ
   t'''\) for some normal \(t'''\). Since \(t'\neq t'''\) or \(t''\neq t'''\), either
\(t_1'\not\in UN\) or \(t_1''\not\in UN\); so take \(t_1:=t_1'\) if \(t'\neq t'''\),
\(t_1:=t_1''\) otherwise.

Hence we can always find a \(t_1\prec t\) with \(t_1\not\in UN\) and get an
infinite sequence contradicting the SN of \(t\)
\end{proof}

\begin{definition}[]
The \textbf{simple typed lambda calculus} \(\blambda_{\bto}\) is the calculus of
\(\beta\)-reduction and \(\beta\)-equality on the set of terms of \(\blambda_{\bto}\).
\(\blambda_{\bto}\) has the term system as described with the following axioms and
rules for \(\prec\) (\(\prec_\beta\)) and \(=\) (is \(=_\beta\))
\begin{align*}
&t\succeq t\quad(\lambda x^A.t^B)s^A\succeq t^B[x^A/s^A]\\
&\frac{t\succeq s}{rt\succeq rs}\quad
\frac{t\succ s}{tr\succ sr}\quad
\frac{t\succeq s}{\lambda x.t\succeq\lambda x.s}\quad
\frac{t\succeq s\quad s\succeq r}{t\succeq r}\\
&\frac{t\succeq s}{t=s}\quad\frac{t=s}{s=t}\quad
\frac{t=s\quad s=r}{t=r}
\end{align*}
The \textbf{extensional simple typed lambda calculus} \(\blambda\boldeta_\to\) is the
calculus of \(\beta \eta\)-reduction and \(\beta \eta\)-equality and the ser of terms
of \(\blambda_{\bto}\); in addition there is the axiom
\begin{equation*}
\lambda x.tx\succeq t\quad(x\not\in\fv(t))
\end{equation*}
\end{definition}

\begin{lemma}[Substitutivity of $\succ_\beta$ and $\succ_{\beta\eta}$]
For \(\succeq\) either \(\succeq_\beta\) or \(\succ_{\beta\eta}\) we have
\begin{equation*}
\text{if } s\succeq s' \text{ then } s[y/s'']\succeq s'[y/s'']
\end{equation*}
\end{lemma}
\begin{proof}
By induction on the depth of a proof of \(s\succeq s'\). It suffices to check
the crucial basis step, where \(s\) is \((\lambda x.t)t'\) and \(s'\) is \(t[x/t']\).
\begin{equation*}
(\lambda x.t)t'[y/s'']=(\lambda x.(t[y/s''])t'[y/s''])=
t[y/s''][x/t'[y/s'']]=t[x/t'][y/s'']
\end{equation*}
\end{proof}

\begin{proposition}[]
\(\succ_{\beta,1}\) and \(\succ_{\beta\eta,1}\) are weakly confluent
\end{proposition}
\begin{proof}
If the conversions leading from \(t\) to \(t'\) and \(t\) to \(t''\) concern disjoint
redexes, then \(t'''\) is simply obtained by converting both redexes

If \(t\equiv\dots(\lambda x.s)s'\dots\), \(t'\equiv\dots s[x/s']\dots\) and
\(t''\equiv\dots(\lambda x.s)s''\dots\), \(s'\succ_1 s''\), then \(t'''\equiv\dots
   s[x/s'']\dots\) and \(t'\succeq t'''\)  
in as many steps as there are occurrences of \(x\) in \(s\), hence \emph{weak}

If \(t\equiv\dots(\lambda x.s)s'\dots\), \(t'\equiv\dots s[x/s']\dots\) and
\(t''\equiv\dots(\lambda x.s'')s'\dots\), \(s\succ_1 s''\), then \(t'''\equiv\dots
   s''[x/s']\dots\)

If \(t\equiv\dots(\lambda x.sx)s'\), \(t'=\dots (sx)[x/s']\dots\),
\(t''\equal\dots ss'\dots\)
\end{proof}

\begin{theorem}[]
The terms of \(\blambda_{\bto},\blambda\boldeta_{\bto}\) are SN for \(\succeq_\beta\) and
\(\succeq_{\beta\eta}\) respectively, then hence the \(\beta\)- and
\(\beta \eta\)-normal forms are unique
\end{theorem}

From the preceding theorem it follows that the reduction relations are
confluent. This can also be proved directly, without relying on strong
normalization, by the following method, due to W. W. Tait and P. Martin-Löf
(see Barendregt [1984, 3.2]) which also applies to the untyped lambda calculus.
The idea is to prove confluence for a relation \(\succeq_p\) which intuitively
corresponds to conversion of a finite set of redexes such that in case of
nesting the 
inner redexes are converted before the outer ones.
\begin{definition}[]
\(\succeq_p\) on \(\blambda_{\bto}\) is generated by the axiom and rules
\begin{alignat*}{2}
&(\text{id})x\succeq_p x\\
&(\lambda\text{mon})\frac{t\succeq_p t'}{\lambda x.t\succeq_p \lambda x.t'}&&
(\text{appmon})\frac{t\succeq_p t'\quad s\succeq_p s'}{ts\succeq_p t's'}\\
&(\beta\text{par})\frac{t\succeq_p t'\quad s\succeq_ps'}{(\lambda x.t)s\succeq_pt'[x/s']}
&&(\eta\text{par})\frac{t\succeq_p t'}{\lambda x.tx\succeq_pt'}
(x\not\in\fv(t))
\end{alignat*}
\end{definition}

\begin{lemma}[Substitutivity of $\succ_p$]
If \(t\succ_p t',s\succ_p s'\), then \(t[x/s]\succ_p t'[x/s']\)
\end{lemma}

\begin{proof}
By induction on \(t\). Assume, w.l.o.g., \(x\not\in\fv(s)\)

\begin{enumerate}
\item \(t\equiv(\lambda y.t_1)t_2\), then
\begin{align*}
&t\succeq_p t_1'[y/t_2']\\
&t[x/s]\equiv(\lambda y.t_1[x/s])t_2[x/s]\succeq_p
t_1'[x/s'][y/t_2'[x/s']]\equiv
t_1'[y/t_2'][x/s']
\end{align*}
\item \(t\equiv\lambda x.t_1x\)
\end{enumerate}
\end{proof}

\begin{lemma}[]
\(\succeq_p\) is confluent
\end{lemma}

\begin{proof}
Induction on \(t\)
\end{proof}

\begin{theorem}[]
\(\beta\)- and \(\beta \eta\)-reduction are confluent
\end{theorem}
\begin{proof}
The reflexive closure of \(\succ_1\) for \(\beta \eta\)-reduction is contained in
\(\succeq_p\), and \(\succeq\) is therefore the transitive closure of
\(\succeq_p\). Write \(t\succeq_{p,n}t'\) if there is a chain
\(t\equiv t_0\succeq_p t_1\succeq_p\dots\succeq_pt_n\equiv t'\). Then we show
by induction on \(n+m\) using the preceding lemma, that if
\(t\succeq_{p,n}t',t\succeq_{p,m}t''\) then there is a \(t'''\) s.t.
\(t'\succeq_{p,m}t''',t''\succeq_{p,n}t'''\) 
\begin{center}
\begin{tikzcd}
t \arrow[r,"\alpha-1"] \arrow[rd,"n+m+1-\alpha"{left}]&
t_0' \arrow[r,"1"] \arrow[rd,"n+m+1-\alpha"]&
t' \arrow[rd]\\
&t'' \arrow[r,"\alpha-1"] &
t_0''' \arrow[r]&t'''
\end{tikzcd}
\end{center}
\end{proof}

\begin{definition}[Terms of typed combinatory logic $\cl_\to$]
The terms are inductive defined as in the case of \(\blambda_{\bto}\), but now with
the clauses
\begin{enumerate}
\item For each \(A\in\calt_\to\) there is a countably infinite supply of variables
of type \(A\); for arbitrary variables of type \(A\) we use
\(u^A,v^A,w^A,x^A,y^A,z^A\)
\item for each \(A,B,C\in\calt\) there are constant terms
\begin{align*}
&\bk^{A,B}\in A\to(B\to A)\\
&\bs^{A,B,C}\in (A\to(B\to C))\to((A\to B)\to(A\to C))
\end{align*}
\item if \(t^{A,B},s^A\) are terms, then so is \(t^{A,B}s\)
\end{enumerate}


\(\fv(\bk)=\fv(\bs)=\emptyset\)
\end{definition}

\begin{definition}[]
The \textbf{weak reduction} relation \(\succeq_w\) on the terms of \(\cl_\to\) is
generated by a conversion relation \(\cont_w\) consisting of the following
pairs
\begin{equation*}
\bk^{A,B}x^Ay^B\e\cont_w\e x,\quad\bs^{A,B,C}x^{A\to(B\to C)}y^{A\to B}z^A
\e\cont_w\e xz(yz)
\end{equation*}

In otherwords, \(\cl_\to\) is the term system defined above with the following
axioms and rules for \(\succeq_w\) and \(=_w\)
\begin{alignat*}{3}
&t\succeq t&&\bk xy\succeq x\quad&&\bs xyz\succeq xz(yz)\\
&\frac{t\succeq s}{rt\succeq rs}\quad&&\frac{t\succeq s}{tr\succeq sr}&&
\frac{t\succeq s\quad s\succeq r}{t\succeq r}\\
&\frac{t\succeq s}{t=s}&&\frac{t=s}{s=t}&&\frac{t=s\quad s=r}{t=r}
\end{alignat*}
\end{definition}

\begin{theorem}[]
The weak reduction relation in \(\cl_\to\), is confluent and
strongly normalizing, so normal forms are unique.
\end{theorem}

\begin{theorem}[]
To each term \(t\) in \(\cl_\to\), there is another term \(\lambda^*x^A.t\) such
that
\begin{enumerate}
\item \(x^A\not\in\fv(\lambda^*x^A.t)\)
\item \((\lambda^*x^A.t)s^A\succ_wt[x^A/s^A]\)
\end{enumerate}
\end{theorem}
\begin{proof}
\begin{align*}
&\lambda^*x^A.x:=\bs^{A,A\to A,A}\bk^{A,A\to A}\bk^{A,A}\\
&\lambda^*x^A.y^B:=\bk^{B,A}y^B\text{ for }y\not\equiv x\\
&\lambda^*x^A.t_1^{B\to C}t_2^B:=\bs^{A,B,C}(\lambda^*x.t_1)(\lambda^*x.t_2)
\end{align*}
\end{proof}

\begin{corollary}[]
\(\cl_\to\) is \textbf{combinatorially complete}, i.e. for every applicative
combination \(t\) of \(\bk,\bs\) and variables \(x_1,x_2,\dots x_n\) there is a
closed term \(s\) s.t. in \(\cl_\to\vdash sx_1\dots x_n=_w t\), in fact even
\(\cl_\to\vdash sx_1\dots x_n\succeq_w t\)
\end{corollary}

\begin{remark}
Note that: it's not true that if \(t=t'\) then \(\lambda^*x.t=\lambda^*x.t'\). 
\(\bk x\bk=x\) but \(\lambda^*x.\bk x\bk=\bs(\bs(\bk\bk)(\bs\bk\bk))(\bk\bk)\),
\(\lambda^*x.x=\bs\bk\bk\)
\end{remark}

\begin{definition}[]
The \textbf{Church numerals} of type \(A\) are \(\beta\)-normal terms \(\bar{n}_A\) of type 
\((A\to A)\to(A\to A), n\in\N\), defined by
\begin{equation*}
\bar{n}_A:=\lambda f^{A\to A}\lambda x^A.f^n(x)
\end{equation*}
where \(f^0(x):=x,f^{n+1}(x):=f(f^n(x))\). \(N_A=\{\bar{n}_A\}\)
\end{definition}
N.B. If we want to use \(\beta \eta\)-normal terms, we must use \(\lambda f^{A\to
   A}.f\) instead of \(\lambda fx.fx\) for \(\bar{1}_A\)

\begin{definition}[]
A function ff\(f:\N^k\to\N\) is said to be \textbf{A-representable} if there is a term \(F\)
of \(\blambda_{\bto}\) s.t. (abbreviating \(\bar{n}_A\) as \(\bar{n}\))
\begin{equation*}
F\bar{n}_1\dots\bar{n}_k=\bar{f(n_1,\dots,n_k)}
\end{equation*}
for all \(n_1,\dots,n_k\in\N,\bar{n}_i=(\bar{n}_i)_A\)
\end{definition}


\begin{definition}[]
\textbf{Polynomials}, \textbf{extended polynomials}
\begin{enumerate}
\item The \(n\)-argument \textbf{projections} \(\bp_i^n\) are given by
\(\bp_i^n(x_1,\dots,x_n)=x_i\), the unary constant functions \(\bc_m\) by
\(\bc_m(x)=m\), and \(\sg\), \(\overline{\sg}\) are unary functions which satisfy
\(\sg(S_n)=1\), \(\sg(0)=0\), where \(S\) is the successor function.
\item The \(n\)-argument function \(f\) is the \textbf{composition} of \(m\)-argument \(g\),
\(n\)-argument \(h_1,\dots,h_m\) if \(f\) satisfies
\(f(\bar{x})=g(h_1(\bar{x}),\dots,h_m(\bar{x}))\)
\item The \textbf{polynomials} in \(n\) variables are generated from \(\bp_i^n,\bc_m\),
addition and multiplication by closure under composition. The \textbf{extended
polynomials} are generated from \(\bp_i^n,\bc_m,\sg,\bar{sg}\), addition and
multiplication by closure under proposition
\end{enumerate}
\end{definition}

\begin{exercise}
Show that all terms in \(\beta\)-normal form of type \((P\to P)\to(P\to P)\), \(P\) a
propositional variable, are either of the form \(\bar{n}_P\) or of the form
\(\lambda f^{P\to P}.f\)
\end{exercise}
\begin{proof}
\begin{enumerate}
\item \(\lambda f^{P\to P}\lambda x^P.t^P\) and \(t\) is in \(\beta\)-normal form.
\item \(\lambda f^{P\to P}.f\)
\end{enumerate}
\end{proof}

\begin{theorem}[]
All extended polynomials are representable in \(\blambda_{\bto}\)
\end{theorem}
\begin{proof}
Abbreviate \(\N_A\) as \(N\).
\begin{alignat*}{2}
&F_+&&:=\lambda x^Ny^Nf^{A\to A}z^A.xf(yfz)\\
&F_\times&&:=\lambda x^Ny^Nf^{A\to A}.x(yf)\\
&F_{\bp_i^k}&&:=\lambda x_1^N\dots x_k^N.x_i\\
&F_{\bc_n}&&:=\lambda x^N.\overline{n}\\
&F_{\sg}&&:=\lambda x^Nf^{A\to A}z^A.x(\lambda u^A.fz)z\\
&F_{\overline{\sg}}&&:=\lambda x^Nf^{A\to A}z^A.x(\lambda u^A.z)(fz)
\end{alignat*}
\end{proof}

\subsection{Three Types of Formalism}
\label{sec:org0df50f9}
\subsubsection{The BHK-interpretation}
\label{sec:org18eae51}
Minimal logic and intuitionistic logic differ only in the treatment of
negation, or (equivalently) falsehood, and minimal implication logic is the
same  
as intuitionistic implication logic

The informal interpretation underlying intuitionistic logic is the
Brouwer-Heyting-Kolmogorov interpretation; this interpretation tells us what
it means to 
prove a compound statement such as \(A\to B\) in terms of what it means to
prove the components \(B\) and \(A\) 
\begin{align*}
&\text{A construction }p\text{ proves }A\to B\text{ if }p\text{ transforms any
possible proof }q\\
&\text{of }A\text{ into a proof }p(q)\text{ of }B
\end{align*}

A \textbf{logical law} of implication logic, according to the BHK-interpretation, is a
formula for which we can give a proof, no matter how we interpret the atomic
formulas. A \textbf{rule} is valid for this interpretation if we know how to construct
a proof for the conclusion, given proofs of the premises

The following two rules for \(\to\) are obviously valid on the basis of the
BHK-interpretation: 
\begin{enumerate}
\item If, starting from a hypothetical (unspecified) proof \(u\) of \(A\), we can find
a proof \(t(u)\) of B, then we have in fact given a proof of \(A\to B\) (without
the assumption that \(u\) proves \(A\)). This proof may be denoted by
\(\lambda u.t(u)\).
\item Given a proof \(t\) of \(A\to B\), and a proof \(s\) of A, we can apply \(t\) to \(s\)
to obtain a proof of \(B\). For this proof we may write \(\app(t,s)\) or \(ts\) (\(t\)
applied to \(s\)).
\end{enumerate}
\subsubsection{A natural deduction system for minimal implication logic}
\label{sec:org49c0238}
Characteristic for natural deduction is the use of assumptions which may
be \textbf{closed} at some later step in the deduction.

The assumptions in a deduction which are occurrences of the same formula
with the same marker form together an \textbf{assumption class}. The notations
\begin{alignat*}{4}
&[A]^u\e\e&&A^u\e\e&&\cald'\e\e&&\cald'\\
&\cald&&\cald&&[A]&&A\\
&B&&B&&\cald&&\cald\\
& && &&B&&B
\end{alignat*}
have the following meaning, from left to right: 
\begin{enumerate}
\item a deduction \(\cald\), with
conclusion \(B\) and a set \([A]\) of open assumptions, consisting of all
occurrences of 
the formula \(A\) at top nodes of the prooftree \(\cald\) with marker \(u\) (note: both \(B\)
and the \([A]\) are part of \(\cald\), and we do not talk about the \textbf{multiset} \([A]^u\) since
we are dealing with formula occurrences);
\item a deduction \(\cald\), with conclusion
\(B\) and a single assumption of the form \(A\) marked \(u\) occurring at some top
node;
\item deduction \(\cald\) with a deduction \(\cald'\), with conclusion \(A\), substituted
for the assumptions \([A]^u\) of \(\cald\); (4) the same, but now for a single assumption
occurrence \(A\) in \(\cald\).
\item the formula \(A\) shown is the conclusion of \(\cald'\)
as well as the formula in an assumption class of \(\cald\).
\end{enumerate}


We now consider a system \(\tonm\) for the minimal theory of implication.

A single formula occurrence \(A\) labelled with a marker is a single-node
prooftree, representing a deduction with conclusion A from open assumption
A.




\begin{figure}
\centering
\begin{subfigure}[h]{0.3\textwidth}
\begin{prooftree}
\AxiomC{$[A]^u$}
\noLine
\UnaryInfC{$\cald$}
\noLine
\UnaryInfC{$B$}
\RightLabel{${\to}$I$,u$}
\UnaryInfC{$A\to B$}
\end{prooftree}
\end{subfigure}

\begin{subfigure}[h]{0.3\textwidth}
\begin{prooftree}
\AxiomC{$\cald$}
\noLine
\UnaryInfC{$A\to B$}
\AxiomC{$\cald'$}
\noLine
\UnaryInfC{$A$}
\RightLabel{${\to}$E}
\BinaryInfC{$B$}
\end{prooftree}
\end{subfigure}
\end{figure}
\end{document}
\end{document}